es:ES, P:(E), R:(EE).
single-thread-generator{i:l}(es;P;R)
 (connex({e:E| P(e)} ;R^*)
 c (R^+|P <>{E} x,y:E. (x < y)|P)
 c (R|P^+ <>{E} R^+|P)
 c (R|P <>{E} R|P^+!)
 c (x, y, x', y':E. (R|P^+(x,y))  (R|P(y',y))  ((R|P^*)(x,y')))
 c (x, y, x', y':E. (R|P^+(x,y))  (R|P(x',x))  (R|P(y',y))  (R|P^+(x',y')))) 

latex

Definitions	ES, , Type, x:A. B(x), R!, E <>{T} E', x,y:T. E(x;y), (e < e'), R|P, R^+, connex(T;R), R^*, {x:A| B(x)} , x(s), f(a), E, single-thread-generator{i:l}(es;P;R), P  Q, x:AB(x), x:A  B(x), A c B, Dec(P), P & Q, Connex(T;x,y.R(x;y)), t  T, P  Q, left + right, SqStable(P), T, True, P  Q, P  Q, x f y, s = t, e < e', t.1, R1 => R2, b
Lemmas	rel-restriction wf, es-causl wf, rel plus wf, rel star wf, rel-star-iff-rel-plus-or, or functionality wrt iff, sq stable from decidable, generated-thread-properties